'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, top(mark(X)) -> top(proper(X))
, top(ok(X)) -> top(active(X))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ active^#(zeros()) -> c_0(cons^#(0(), zeros()))
, active^#(tail(cons(X, XS))) -> c_1()
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, active^#(tail(X)) -> c_3(tail^#(active(X)))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))
, tail^#(mark(X)) -> c_5(tail^#(X))
, proper^#(zeros()) -> c_6()
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, proper^#(0()) -> c_8()
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))
, top^#(mark(X)) -> c_12(top^#(proper(X)))
, top^#(ok(X)) -> c_13(top^#(active(X)))}
The usable rules are:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
The estimated dependency graph contains the following edges:
{active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
==> {cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
{active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
==> {cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
{active^#(tail(X)) -> c_3(tail^#(active(X)))}
==> {tail^#(ok(X)) -> c_11(tail^#(X))}
{active^#(tail(X)) -> c_3(tail^#(active(X)))}
==> {tail^#(mark(X)) -> c_5(tail^#(X))}
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
==> {cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
==> {cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
{tail^#(mark(X)) -> c_5(tail^#(X))}
==> {tail^#(ok(X)) -> c_11(tail^#(X))}
{tail^#(mark(X)) -> c_5(tail^#(X))}
==> {tail^#(mark(X)) -> c_5(tail^#(X))}
{proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
==> {cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
{proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
==> {cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
{proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
==> {tail^#(ok(X)) -> c_11(tail^#(X))}
{proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
==> {tail^#(mark(X)) -> c_5(tail^#(X))}
{cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
==> {cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
{cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
==> {cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
{tail^#(ok(X)) -> c_11(tail^#(X))}
==> {tail^#(ok(X)) -> c_11(tail^#(X))}
{tail^#(ok(X)) -> c_11(tail^#(X))}
==> {tail^#(mark(X)) -> c_5(tail^#(X))}
{top^#(mark(X)) -> c_12(top^#(proper(X)))}
==> {top^#(ok(X)) -> c_13(top^#(active(X)))}
{top^#(mark(X)) -> c_12(top^#(proper(X)))}
==> {top^#(mark(X)) -> c_12(top^#(proper(X)))}
{top^#(ok(X)) -> c_13(top^#(active(X)))}
==> {top^#(ok(X)) -> c_13(top^#(active(X)))}
{top^#(ok(X)) -> c_13(top^#(active(X)))}
==> {top^#(mark(X)) -> c_12(top^#(proper(X)))}
We consider the following path(s):
1) { top^#(mark(X)) -> c_12(top^#(proper(X)))
, top^#(ok(X)) -> c_13(top^#(active(X)))}
The usable rules for this path are the following:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, top^#(mark(X)) -> c_12(top^#(proper(X)))
, top^#(ok(X)) -> c_13(top^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [9]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [1] x1 + [15]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{top^#(ok(X)) -> c_13(top^#(active(X)))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{top^#(ok(X)) -> c_13(top^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [12]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_12(x1) = [1] x1 + [1]
c_13(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(tail(cons(X, XS))) -> mark(XS)}
and weakly orienting the rules
{ top^#(ok(X)) -> c_13(top^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(tail(cons(X, XS))) -> mark(XS)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [8]
proper(x1) = [1] x1 + [0]
ok(x1) = [1] x1 + [10]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [11]
c_12(x1) = [1] x1 + [0]
c_13(x1) = [1] x1 + [1]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
and weakly orienting the rules
{ active(tail(cons(X, XS))) -> mark(XS)
, top^#(ok(X)) -> c_13(top^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [8]
cons(x1, x2) = [1] x1 + [1] x2 + [8]
0() = [6]
tail(x1) = [1] x1 + [4]
proper(x1) = [1] x1 + [2]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [1] x1 + [0]
c_12(x1) = [1] x1 + [1]
c_13(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, active(tail(cons(X, XS))) -> mark(XS)
, top^#(ok(X)) -> c_13(top^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, active(tail(cons(X, XS))) -> mark(XS)
, top^#(ok(X)) -> c_13(top^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, top^#(mark(X)) -> c_12(top^#(proper(X)))}
Details:
The problem is Match-bounded by 4.
The enriched problem is compatible with the following automaton:
{ active_0(2) -> 28
, active_0(3) -> 28
, active_0(5) -> 28
, active_0(8) -> 28
, active_1(2) -> 35
, active_1(3) -> 35
, active_1(5) -> 35
, active_1(8) -> 35
, active_2(32) -> 45
, active_2(33) -> 45
, active_2(46) -> 50
, active_3(43) -> 53
, active_3(46) -> 59
, active_3(60) -> 64
, active_4(57) -> 65
, active_4(60) -> 67
, zeros_0() -> 2
, zeros_1() -> 33
, zeros_2() -> 42
, zeros_3() -> 56
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, mark_1(31) -> 28
, mark_1(31) -> 35
, mark_2(46) -> 45
, cons_1(32, 33) -> 31
, cons_2(40, 41) -> 39
, cons_2(40, 41) -> 48
, cons_2(43, 42) -> 46
, cons_3(53, 42) -> 50
, cons_3(53, 42) -> 59
, cons_3(54, 55) -> 52
, cons_3(54, 55) -> 62
, cons_3(57, 56) -> 60
, cons_4(65, 56) -> 64
, cons_4(65, 56) -> 67
, 0_0() -> 5
, 0_1() -> 32
, 0_2() -> 43
, 0_3() -> 57
, proper_0(2) -> 30
, proper_0(3) -> 30
, proper_0(5) -> 30
, proper_0(8) -> 30
, proper_1(2) -> 37
, proper_1(3) -> 37
, proper_1(5) -> 37
, proper_1(8) -> 37
, proper_1(31) -> 39
, proper_2(31) -> 48
, proper_2(32) -> 40
, proper_2(33) -> 41
, proper_2(46) -> 52
, proper_3(42) -> 55
, proper_3(43) -> 54
, proper_3(46) -> 62
, ok_0(2) -> 8
, ok_0(2) -> 30
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(5) -> 30
, ok_0(8) -> 8
, ok_1(32) -> 37
, ok_1(33) -> 37
, ok_2(42) -> 41
, ok_2(43) -> 40
, ok_2(46) -> 39
, ok_2(46) -> 48
, ok_3(56) -> 55
, ok_3(57) -> 54
, ok_3(60) -> 52
, ok_3(60) -> 62
, top^#_0(2) -> 26
, top^#_0(3) -> 26
, top^#_0(5) -> 26
, top^#_0(8) -> 26
, top^#_0(28) -> 27
, top^#_0(30) -> 29
, top^#_1(35) -> 34
, top^#_1(37) -> 36
, top^#_1(39) -> 38
, top^#_2(45) -> 44
, top^#_2(48) -> 47
, top^#_2(50) -> 49
, top^#_2(52) -> 51
, top^#_3(59) -> 58
, top^#_3(62) -> 61
, top^#_3(64) -> 63
, top^#_4(67) -> 66
, c_12_0(29) -> 26
, c_12_1(36) -> 26
, c_12_1(38) -> 27
, c_12_2(47) -> 34
, c_12_2(51) -> 44
, c_12_3(61) -> 44
, c_13_0(27) -> 26
, c_13_1(34) -> 26
, c_13_1(34) -> 29
, c_13_2(44) -> 36
, c_13_2(49) -> 38
, c_13_3(58) -> 47
, c_13_3(63) -> 51
, c_13_4(66) -> 61}
2) { active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
The usable rules for this path are the following:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [7]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
and weakly orienting the rules
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [3]
c_1() = [0]
c_2(x1) = [1] x1 + [2]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
and weakly orienting the rules
{ active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [7]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [4]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [6]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(tail(cons(X, XS))) -> mark(XS)}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(tail(cons(X, XS))) -> mark(XS)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [1]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [8]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(zeros()) -> mark(cons(0(), zeros()))}
and weakly orienting the rules
{ active(tail(cons(X, XS))) -> mark(XS)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(zeros()) -> mark(cons(0(), zeros()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [4]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [2]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, active^#_0(2) -> 10
, active^#_0(3) -> 10
, active^#_0(5) -> 10
, active^#_0(8) -> 10
, cons^#_0(2, 2) -> 12
, cons^#_0(2, 3) -> 12
, cons^#_0(2, 5) -> 12
, cons^#_0(2, 8) -> 12
, cons^#_0(3, 2) -> 12
, cons^#_0(3, 3) -> 12
, cons^#_0(3, 5) -> 12
, cons^#_0(3, 8) -> 12
, cons^#_0(5, 2) -> 12
, cons^#_0(5, 3) -> 12
, cons^#_0(5, 5) -> 12
, cons^#_0(5, 8) -> 12
, cons^#_0(8, 2) -> 12
, cons^#_0(8, 3) -> 12
, cons^#_0(8, 5) -> 12
, cons^#_0(8, 8) -> 12
, c_4_0(12) -> 12
, c_10_0(12) -> 12}
3) { active^#(tail(X)) -> c_3(tail^#(active(X)))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
The usable rules for this path are the following:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, active^#(tail(X)) -> c_3(tail^#(active(X)))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{tail^#(mark(X)) -> c_5(tail^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{tail^#(mark(X)) -> c_5(tail^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
and weakly orienting the rules
{tail^#(mark(X)) -> c_5(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [6]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(tail(X)) -> c_3(tail^#(active(X)))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(tail(X)) -> c_3(tail^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [2]
tail^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(tail(cons(X, XS))) -> mark(XS)}
and weakly orienting the rules
{ active^#(tail(X)) -> c_3(tail^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(tail(cons(X, XS))) -> mark(XS)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [4]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [13]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [1]
tail^#(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(zeros()) -> mark(cons(0(), zeros()))}
and weakly orienting the rules
{ active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(zeros()) -> mark(cons(0(), zeros()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
tail^#(x1) = [1] x1 + [6]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, active^#_0(2) -> 10
, active^#_0(3) -> 10
, active^#_0(5) -> 10
, active^#_0(8) -> 10
, tail^#_0(2) -> 16
, tail^#_0(3) -> 16
, tail^#_0(5) -> 16
, tail^#_0(8) -> 16
, c_5_0(16) -> 16
, c_11_0(16) -> 16}
4) { proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
The usable rules for this path are the following:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7(x1) = [1] x1 + [1]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_6() = [0]
c_7(x1) = [1] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
and weakly orienting the rules
{ proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [8]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [8]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [13]
c_6() = [0]
c_7(x1) = [1] x1 + [1]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [2]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
and weakly orienting the rules
{ cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [7]
c_6() = [0]
c_7(x1) = [1] x1 + [1]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, cons^#(mark(X1), X2) -> c_4(cons^#(X1, X2))
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, cons^#(ok(X1), ok(X2)) -> c_10(cons^#(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, cons^#_0(2, 2) -> 12
, cons^#_0(2, 3) -> 12
, cons^#_0(2, 5) -> 12
, cons^#_0(2, 8) -> 12
, cons^#_0(3, 2) -> 12
, cons^#_0(3, 3) -> 12
, cons^#_0(3, 5) -> 12
, cons^#_0(3, 8) -> 12
, cons^#_0(5, 2) -> 12
, cons^#_0(5, 3) -> 12
, cons^#_0(5, 5) -> 12
, cons^#_0(5, 8) -> 12
, cons^#_0(8, 2) -> 12
, cons^#_0(8, 3) -> 12
, cons^#_0(8, 5) -> 12
, cons^#_0(8, 8) -> 12
, c_4_0(12) -> 12
, proper^#_0(2) -> 19
, proper^#_0(3) -> 19
, proper^#_0(5) -> 19
, proper^#_0(8) -> 19
, c_10_0(12) -> 12}
5) { proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
The usable rules for this path are the following:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, tail^#(ok(X)) -> c_11(tail^#(X))
, tail^#(mark(X)) -> c_5(tail^#(X))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [2]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [7]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [4]
proper^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [8]
proper^#(x1) = [1] x1 + [3]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{tail^#(mark(X)) -> c_5(tail^#(X))}
and weakly orienting the rules
{ proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{tail^#(mark(X)) -> c_5(tail^#(X))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [4]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [12]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [13]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
and weakly orienting the rules
{ tail^#(mark(X)) -> c_5(tail^#(X))
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [15]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
proper^#(x1) = [1] x1 + [5]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, tail^#(mark(X)) -> c_5(tail^#(X))
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, tail^#(mark(X)) -> c_5(tail^#(X))
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail^#(ok(X)) -> c_11(tail^#(X))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, tail^#_0(2) -> 16
, tail^#_0(3) -> 16
, tail^#_0(5) -> 16
, tail^#_0(8) -> 16
, c_5_0(16) -> 16
, proper^#_0(2) -> 19
, proper^#_0(3) -> 19
, proper^#_0(5) -> 19
, proper^#_0(8) -> 19
, c_11_0(16) -> 16}
6) {active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
The usable rules for this path are the following:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [2]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [15]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [1]
c_1() = [0]
c_2(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(tail(cons(X, XS))) -> mark(XS)}
and weakly orienting the rules
{ active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(tail(cons(X, XS))) -> mark(XS)}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [8]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(zeros()) -> mark(cons(0(), zeros()))}
and weakly orienting the rules
{ active(tail(cons(X, XS))) -> mark(XS)
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(zeros()) -> mark(cons(0(), zeros()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, active^#_0(2) -> 10
, active^#_0(3) -> 10
, active^#_0(5) -> 10
, active^#_0(8) -> 10
, cons^#_0(2, 2) -> 12
, cons^#_0(2, 3) -> 12
, cons^#_0(2, 5) -> 12
, cons^#_0(2, 8) -> 12
, cons^#_0(3, 2) -> 12
, cons^#_0(3, 3) -> 12
, cons^#_0(3, 5) -> 12
, cons^#_0(3, 8) -> 12
, cons^#_0(5, 2) -> 12
, cons^#_0(5, 3) -> 12
, cons^#_0(5, 5) -> 12
, cons^#_0(5, 8) -> 12
, cons^#_0(8, 2) -> 12
, cons^#_0(8, 3) -> 12
, cons^#_0(8, 5) -> 12
, cons^#_0(8, 8) -> 12}
7) {active^#(tail(X)) -> c_3(tail^#(active(X)))}
The usable rules for this path are the following:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, active(tail(cons(X, XS))) -> mark(XS)
, active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [4]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{ active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [1]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [8]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{active(zeros()) -> mark(cons(0(), zeros()))}
and weakly orienting the rules
{ cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active(zeros()) -> mark(cons(0(), zeros()))}
Details:
Interpretation Functions:
active(x1) = [1] x1 + [1]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [1] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ active(cons(X1, X2)) -> cons(active(X1), X2)
, active(tail(X)) -> tail(active(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ active(zeros()) -> mark(cons(0(), zeros()))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, active(tail(cons(X, XS))) -> mark(XS)
, active^#(tail(X)) -> c_3(tail^#(active(X)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, active^#_0(2) -> 10
, active^#_0(3) -> 10
, active^#_0(5) -> 10
, active^#_0(8) -> 10
, tail^#_0(2) -> 16
, tail^#_0(3) -> 16
, tail^#_0(5) -> 16
, tail^#_0(8) -> 16}
8) {proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
The usable rules for this path are the following:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [4]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [15]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7(x1) = [1] x1 + [15]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [4]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_6() = [0]
c_7(x1) = [1] x1 + [1]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [1]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [2]
c_6() = [0]
c_7(x1) = [1] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, proper^#(cons(X1, X2)) -> c_7(cons^#(proper(X1), proper(X2)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, cons^#_0(2, 2) -> 12
, cons^#_0(2, 3) -> 12
, cons^#_0(2, 5) -> 12
, cons^#_0(2, 8) -> 12
, cons^#_0(3, 2) -> 12
, cons^#_0(3, 3) -> 12
, cons^#_0(3, 5) -> 12
, cons^#_0(3, 8) -> 12
, cons^#_0(5, 2) -> 12
, cons^#_0(5, 3) -> 12
, cons^#_0(5, 5) -> 12
, cons^#_0(5, 8) -> 12
, cons^#_0(8, 2) -> 12
, cons^#_0(8, 3) -> 12
, cons^#_0(8, 5) -> 12
, cons^#_0(8, 8) -> 12
, proper^#_0(2) -> 19
, proper^#_0(3) -> 19
, proper^#_0(5) -> 19
, proper^#_0(8) -> 19}
9) {proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
The usable rules for this path are the following:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ proper(zeros()) -> ok(zeros())
, proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(0()) -> ok(0())
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))
, tail(ok(X)) -> ok(tail(X))
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
and weakly orienting the rules
{cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(tail(X)) -> c_9(tail^#(proper(X)))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [1]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [9]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
and weakly orienting the rules
{ proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [1] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [1] x1 + [1]
ok(x1) = [1] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [4]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ proper(cons(X1, X2)) -> cons(proper(X1), proper(X2))
, proper(tail(X)) -> tail(proper(X))
, cons(mark(X1), X2) -> mark(cons(X1, X2))
, tail(mark(X)) -> mark(tail(X))
, tail(ok(X)) -> ok(tail(X))}
Weak Rules:
{ proper(zeros()) -> ok(zeros())
, proper(0()) -> ok(0())
, proper^#(tail(X)) -> c_9(tail^#(proper(X)))
, cons(ok(X1), ok(X2)) -> ok(cons(X1, X2))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ zeros_0() -> 2
, mark_0(2) -> 3
, mark_0(3) -> 3
, mark_0(5) -> 3
, mark_0(8) -> 3
, 0_0() -> 5
, ok_0(2) -> 8
, ok_0(3) -> 8
, ok_0(5) -> 8
, ok_0(8) -> 8
, tail^#_0(2) -> 16
, tail^#_0(3) -> 16
, tail^#_0(5) -> 16
, tail^#_0(8) -> 16
, proper^#_0(2) -> 19
, proper^#_0(3) -> 19
, proper^#_0(5) -> 19
, proper^#_0(8) -> 19}
10)
{active^#(zeros()) -> c_0(cons^#(0(), zeros()))}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(zeros()) -> c_0(cons^#(0(), zeros()))}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(zeros()) -> c_0(cons^#(0(), zeros()))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(zeros()) -> c_0(cons^#(0(), zeros()))}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
cons^#(x1, x2) = [1] x1 + [1] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(zeros()) -> c_0(cons^#(0(), zeros()))}
Details:
The given problem does not contain any strict rules
11)
{active^#(tail(cons(X, XS))) -> c_1()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {active^#(tail(cons(X, XS))) -> c_1()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{active^#(tail(cons(X, XS))) -> c_1()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{active^#(tail(cons(X, XS))) -> c_1()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [1] x1 + [1] x2 + [0]
0() = [0]
tail(x1) = [1] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {active^#(tail(cons(X, XS))) -> c_1()}
Details:
The given problem does not contain any strict rules
12)
{proper^#(zeros()) -> c_6()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(zeros()) -> c_6()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(zeros()) -> c_6()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(zeros()) -> c_6()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(zeros()) -> c_6()}
Details:
The given problem does not contain any strict rules
13)
{proper^#(0()) -> c_8()}
The usable rules for this path are empty.
We have oriented the usable rules with the following strongly linear interpretation:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [0] x1 + [0]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
We have applied the subprocessor on the resulting DP-problem:
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {proper^#(0()) -> c_8()}
Weak Rules: {}
Details:
We apply the weight gap principle, strictly orienting the rules
{proper^#(0()) -> c_8()}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{proper^#(0()) -> c_8()}
Details:
Interpretation Functions:
active(x1) = [0] x1 + [0]
zeros() = [0]
mark(x1) = [0] x1 + [0]
cons(x1, x2) = [0] x1 + [0] x2 + [0]
0() = [0]
tail(x1) = [0] x1 + [0]
proper(x1) = [0] x1 + [0]
ok(x1) = [0] x1 + [0]
top(x1) = [0] x1 + [0]
active^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
cons^#(x1, x2) = [0] x1 + [0] x2 + [0]
c_1() = [0]
c_2(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
tail^#(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
proper^#(x1) = [1] x1 + [1]
c_6() = [0]
c_7(x1) = [0] x1 + [0]
c_8() = [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
top^#(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'Empty TRS'
-----------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {}
Weak Rules: {proper^#(0()) -> c_8()}
Details:
The given problem does not contain any strict rules